Например, Бобцов

Формализация языков частично упорядоченных мультимножеств в системе Coq для спецификации слабых моделей памяти

Аннотация:

Предмет исследования. Модели памяти задают семантику многопоточных программ, работающих с разделяемой памятью. В настоящее время эта область активно развивается, создаются новые модели памяти, востребованы новые средства формализации таких моделей, а также способы и средства доказательства их свойств. В работе рассмотрена задача формальной спецификации моделей памяти в системах интерактивного доказательства теорем. Метод. Использован семантический домен языков частично упорядоченных мультимножеств или языков помсетов. Предложен метод кодировки семантического домена с помощью фактор-типов и обсуждены его достоинства и недостатки. Основные результаты. Представлена библиотека, разработанная в системе Coq, реализующая предложенный метод. В рамках библиотеки установлена взаимосвязь языков помсетов с традиционной операционной семантикой, заданной в терминах помеченных систем переходов. Это позволило специфицировать в Coq модели памяти, параметризованные операционной семантикой структуры данных, и, таким образом, разделить определения модели памяти и структуры данных. Практическая значимость. Предложенная библиотека может быть использована для формальной спецификации и доказательства свойств широкого класса моделей памяти. Чтобы продемонстрировать это, в работе приведена формализация нескольких базовых моделей, а именно, моделей последовательной, причинной и конвейерной согласованности.

Ключевые слова:

Постоянный URL

Статьи в номере

Содержание © 1993–2024 Университет ИТМО
Разработка © 2015 Университет ИТМО